es{-}p{-}immediate{-}pred(${\it es}$;$P$)($e$,${\it e'}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$(${\it e'}$ $<$ $e$) \& $P$($e$) \& $P$(${\it e'}$) \& ($\forall$${\it e''}$:E. (${\it e''}$ $<$ $e$) $\Rightarrow$ (${\it e'}$ $<$ ${\it e''}$) $\Rightarrow$ ($\neg$($P$(${\it e''}$))))